package systemfnomabss
/*
object PrettyTest extends Application {
     val p =   new systemfPrettyPrinter  with AbstractSyntax// { val ctx = new TermContext(Nil) }
     import p._
     println  {prettyPrint(App(Lam("x",TyBool,Var(0)),If(Tru,Fls,Tru))) }
}
     

trait systemfPrettyPrinter extends PrettyPrinter{ self : systemfPrettyPrinter with AbstractSyntax =>
     
   def prettyPrint(t: LTerm):String= PrinterFun.fresh.pretty(t)

   object PrinterFun {
     def fresh() = new PrinterCtxFun {val ctx = new StringBindingContext[NameBinding](Nil)}
   }

   trait PrinterCtxFun extends ContextualFun[LTerm,String,PrinterCtxFun] {
     //def extend(str:String) = extendtransformed(str, {s => pickUniqueName(s)})

     def create(ctxnew: Ctx) = new PrinterCtxFun { val ctx = ctxnew }
     val hintTransform = {s:String => pickUniqueName(s)}
     def onvar(n: Int):String = ctx(n) match {case b:Some[NameBinding] => b.get.name
                                         case None => throw new Exception("printing: no variable name remembered for variable with offset "+n)
                                       }
     def ontyvar(n: Int):String = ctx(n) match {case b:Some[NameBinding] => b.get.name
                                         case None => throw new Exception("printing: no variable name remembered for variable with offset "+n)
                                       }
     def apply(t:LTerm):String = { pretty(t) }

     def pretty(t:LTerm):String = t match {
             case bv:BaseValue         => bv.toString
             case bt:BaseType          => bt.toString
             case If(cond,pos,neg)     => "if "+this(cond) + " then "+this(pos)+" else "+this(neg)
             case Var(n)               => onvar(n)
             case Lam(hint,ty,body)    => "(λ"+pickUniqueName(hint)+":"+this(ty)+" ."+extend(hint)(body)+")"
             case Let(hint, conc, body)   => {
               "let "+pickUniqueName(hint)+" = " +this(conc)+ " in " +extend(hint)(body)
             }
             case App(fun,arg)         => "("+this(fun) + " " + this(arg) + ")"
             
             case Pack(ty, t, pubty)   => "{*"+this(ty)+ ", "+this(t)+" } as "+ this(pubty)
             case Unpack(impl, pubty,pubvar, body)=> {
                 "import " + this(impl)+ "into {"+pickUniqueName(pubty) +", "+pickUniqueName(pubvar) +"} in "+extend(pubty).extend(pubvar)(body)
             }  
               
               
               
             case Record(fields)          => "{" + fields.foldRight("")({case ((s,t),acc) => s +"="+ this(t) +", "+ acc} ) + "}"
             case RecProj(rec,label)      => "from "+ this(rec) + " fld "+label
             case TyArr(ty1, ty2)         => "("+this(ty1)+" => " +this(ty2)+")"
             case TyRecord(fields)        => "{" + fields.foldRight("")({case ((s,t),acc) => s +":"+ this(t) +", "+ acc} )+ "}"
         
             case TyVar(n)              => ontyvar(n)
             case TLam(hint,body)      => "(Λ"+pickUniqueName(hint)+" ."+extend(hint)(body)+")"
             case TApp(tlam, ty: LType)=> "("+this(tlam) +"  [ " +this(ty) + "])"
             case TyUniv(hint,ty)      => "forall "+pickUniqueName(hint)+" ."+extend(hint)(ty)
             case TyExist(x, ty)       => "{forsome "+pickUniqueName(x)+" ,"+extend(x)(ty)+"}"

     
     }
      
   }
  }

*/